FDL - Nuprl Lemma : do-apply-p-restrict

Nuprl Lemma : do-apply-p-restrict

A, B:Type, f:(A

(B + Top)), P:(A

), p:(

x:A. Dec(P(x))), x:A.
(

can-apply(p-restrict(f;p);x))

(do-apply(p-restrict(f;p);x) = do-apply(f;x)

B)

Definitions x:AB(x), P Q, x:A. B(x), x. t(x), f(a), x(s), t T, True, T, Top, left + right, Type, p-filter(f), do-apply(f;x), can-apply(f;x), , , b, P Q, x:A B(x), P & Q, P Q, s = t, Dec(P), p-restrict(f;p)

Lemmas do-apply-compose, can-apply-compose-iff, do-apply wf, assert wf, can-apply wf, do-apply-p-filter